0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 CpxWeightedTrsRenamingProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxWeightedTrs
↳5 InnermostUnusableRulesProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CpxWeightedTrs
↳7 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳8 CpxTypedWeightedTrs
↳9 CompletionProof (UPPER BOUND(ID), 0 ms)
↳10 CpxTypedWeightedCompleteTrs
↳11 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳12 CpxRNTS
↳13 CompleteCoflocoProof (⇔, 6101 ms)
↳14 BOUNDS(1, n^2)
U101(tt, M, N) → U102(isNatKind(activate(M)), activate(M), activate(N))
U102(tt, M, N) → U103(isNat(activate(N)), activate(M), activate(N))
U103(tt, M, N) → U104(isNatKind(activate(N)), activate(M), activate(N))
U104(tt, M, N) → plus(x(activate(N), activate(M)), activate(N))
U11(tt, V1, V2) → U12(isNatKind(activate(V1)), activate(V1), activate(V2))
U12(tt, V1, V2) → U13(isNatKind(activate(V2)), activate(V1), activate(V2))
U13(tt, V1, V2) → U14(isNatKind(activate(V2)), activate(V1), activate(V2))
U14(tt, V1, V2) → U15(isNat(activate(V1)), activate(V2))
U15(tt, V2) → U16(isNat(activate(V2)))
U16(tt) → tt
U21(tt, V1) → U22(isNatKind(activate(V1)), activate(V1))
U22(tt, V1) → U23(isNat(activate(V1)))
U23(tt) → tt
U31(tt, V1, V2) → U32(isNatKind(activate(V1)), activate(V1), activate(V2))
U32(tt, V1, V2) → U33(isNatKind(activate(V2)), activate(V1), activate(V2))
U33(tt, V1, V2) → U34(isNatKind(activate(V2)), activate(V1), activate(V2))
U34(tt, V1, V2) → U35(isNat(activate(V1)), activate(V2))
U35(tt, V2) → U36(isNat(activate(V2)))
U36(tt) → tt
U41(tt, V2) → U42(isNatKind(activate(V2)))
U42(tt) → tt
U51(tt) → tt
U61(tt, V2) → U62(isNatKind(activate(V2)))
U62(tt) → tt
U71(tt, N) → U72(isNatKind(activate(N)), activate(N))
U72(tt, N) → activate(N)
U81(tt, M, N) → U82(isNatKind(activate(M)), activate(M), activate(N))
U82(tt, M, N) → U83(isNat(activate(N)), activate(M), activate(N))
U83(tt, M, N) → U84(isNatKind(activate(N)), activate(M), activate(N))
U84(tt, M, N) → s(plus(activate(N), activate(M)))
U91(tt, N) → U92(isNatKind(activate(N)))
U92(tt) → 0
isNat(n__0) → tt
isNat(n__plus(V1, V2)) → U11(isNatKind(activate(V1)), activate(V1), activate(V2))
isNat(n__s(V1)) → U21(isNatKind(activate(V1)), activate(V1))
isNat(n__x(V1, V2)) → U31(isNatKind(activate(V1)), activate(V1), activate(V2))
isNatKind(n__0) → tt
isNatKind(n__plus(V1, V2)) → U41(isNatKind(activate(V1)), activate(V2))
isNatKind(n__s(V1)) → U51(isNatKind(activate(V1)))
isNatKind(n__x(V1, V2)) → U61(isNatKind(activate(V1)), activate(V2))
plus(N, 0) → U71(isNat(N), N)
plus(N, s(M)) → U81(isNat(M), M, N)
x(N, 0) → U91(isNat(N), N)
x(N, s(M)) → U101(isNat(M), M, N)
0 → n__0
plus(X1, X2) → n__plus(X1, X2)
s(X) → n__s(X)
x(X1, X2) → n__x(X1, X2)
activate(n__0) → 0
activate(n__plus(X1, X2)) → plus(X1, X2)
activate(n__s(X)) → s(X)
activate(n__x(X1, X2)) → x(X1, X2)
activate(X) → X
U101(tt, M, N) → U102(isNatKind(activate(M)), activate(M), activate(N)) [1]
U102(tt, M, N) → U103(isNat(activate(N)), activate(M), activate(N)) [1]
U103(tt, M, N) → U104(isNatKind(activate(N)), activate(M), activate(N)) [1]
U104(tt, M, N) → plus(x(activate(N), activate(M)), activate(N)) [1]
U11(tt, V1, V2) → U12(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
U12(tt, V1, V2) → U13(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U13(tt, V1, V2) → U14(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U14(tt, V1, V2) → U15(isNat(activate(V1)), activate(V2)) [1]
U15(tt, V2) → U16(isNat(activate(V2))) [1]
U16(tt) → tt [1]
U21(tt, V1) → U22(isNatKind(activate(V1)), activate(V1)) [1]
U22(tt, V1) → U23(isNat(activate(V1))) [1]
U23(tt) → tt [1]
U31(tt, V1, V2) → U32(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
U32(tt, V1, V2) → U33(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U33(tt, V1, V2) → U34(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U34(tt, V1, V2) → U35(isNat(activate(V1)), activate(V2)) [1]
U35(tt, V2) → U36(isNat(activate(V2))) [1]
U36(tt) → tt [1]
U41(tt, V2) → U42(isNatKind(activate(V2))) [1]
U42(tt) → tt [1]
U51(tt) → tt [1]
U61(tt, V2) → U62(isNatKind(activate(V2))) [1]
U62(tt) → tt [1]
U71(tt, N) → U72(isNatKind(activate(N)), activate(N)) [1]
U72(tt, N) → activate(N) [1]
U81(tt, M, N) → U82(isNatKind(activate(M)), activate(M), activate(N)) [1]
U82(tt, M, N) → U83(isNat(activate(N)), activate(M), activate(N)) [1]
U83(tt, M, N) → U84(isNatKind(activate(N)), activate(M), activate(N)) [1]
U84(tt, M, N) → s(plus(activate(N), activate(M))) [1]
U91(tt, N) → U92(isNatKind(activate(N))) [1]
U92(tt) → 0 [1]
isNat(n__0) → tt [1]
isNat(n__plus(V1, V2)) → U11(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
isNat(n__s(V1)) → U21(isNatKind(activate(V1)), activate(V1)) [1]
isNat(n__x(V1, V2)) → U31(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
isNatKind(n__0) → tt [1]
isNatKind(n__plus(V1, V2)) → U41(isNatKind(activate(V1)), activate(V2)) [1]
isNatKind(n__s(V1)) → U51(isNatKind(activate(V1))) [1]
isNatKind(n__x(V1, V2)) → U61(isNatKind(activate(V1)), activate(V2)) [1]
plus(N, 0) → U71(isNat(N), N) [1]
plus(N, s(M)) → U81(isNat(M), M, N) [1]
x(N, 0) → U91(isNat(N), N) [1]
x(N, s(M)) → U101(isNat(M), M, N) [1]
0 → n__0 [1]
plus(X1, X2) → n__plus(X1, X2) [1]
s(X) → n__s(X) [1]
x(X1, X2) → n__x(X1, X2) [1]
activate(n__0) → 0 [1]
activate(n__plus(X1, X2)) → plus(X1, X2) [1]
activate(n__s(X)) → s(X) [1]
activate(n__x(X1, X2)) → x(X1, X2) [1]
activate(X) → X [1]
| 0 => 0' |
U101(tt, M, N) → U102(isNatKind(activate(M)), activate(M), activate(N)) [1]
U102(tt, M, N) → U103(isNat(activate(N)), activate(M), activate(N)) [1]
U103(tt, M, N) → U104(isNatKind(activate(N)), activate(M), activate(N)) [1]
U104(tt, M, N) → plus(x(activate(N), activate(M)), activate(N)) [1]
U11(tt, V1, V2) → U12(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
U12(tt, V1, V2) → U13(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U13(tt, V1, V2) → U14(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U14(tt, V1, V2) → U15(isNat(activate(V1)), activate(V2)) [1]
U15(tt, V2) → U16(isNat(activate(V2))) [1]
U16(tt) → tt [1]
U21(tt, V1) → U22(isNatKind(activate(V1)), activate(V1)) [1]
U22(tt, V1) → U23(isNat(activate(V1))) [1]
U23(tt) → tt [1]
U31(tt, V1, V2) → U32(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
U32(tt, V1, V2) → U33(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U33(tt, V1, V2) → U34(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U34(tt, V1, V2) → U35(isNat(activate(V1)), activate(V2)) [1]
U35(tt, V2) → U36(isNat(activate(V2))) [1]
U36(tt) → tt [1]
U41(tt, V2) → U42(isNatKind(activate(V2))) [1]
U42(tt) → tt [1]
U51(tt) → tt [1]
U61(tt, V2) → U62(isNatKind(activate(V2))) [1]
U62(tt) → tt [1]
U71(tt, N) → U72(isNatKind(activate(N)), activate(N)) [1]
U72(tt, N) → activate(N) [1]
U81(tt, M, N) → U82(isNatKind(activate(M)), activate(M), activate(N)) [1]
U82(tt, M, N) → U83(isNat(activate(N)), activate(M), activate(N)) [1]
U83(tt, M, N) → U84(isNatKind(activate(N)), activate(M), activate(N)) [1]
U84(tt, M, N) → s(plus(activate(N), activate(M))) [1]
U91(tt, N) → U92(isNatKind(activate(N))) [1]
U92(tt) → 0' [1]
isNat(n__0) → tt [1]
isNat(n__plus(V1, V2)) → U11(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
isNat(n__s(V1)) → U21(isNatKind(activate(V1)), activate(V1)) [1]
isNat(n__x(V1, V2)) → U31(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
isNatKind(n__0) → tt [1]
isNatKind(n__plus(V1, V2)) → U41(isNatKind(activate(V1)), activate(V2)) [1]
isNatKind(n__s(V1)) → U51(isNatKind(activate(V1))) [1]
isNatKind(n__x(V1, V2)) → U61(isNatKind(activate(V1)), activate(V2)) [1]
plus(N, 0') → U71(isNat(N), N) [1]
plus(N, s(M)) → U81(isNat(M), M, N) [1]
x(N, 0') → U91(isNat(N), N) [1]
x(N, s(M)) → U101(isNat(M), M, N) [1]
0' → n__0 [1]
plus(X1, X2) → n__plus(X1, X2) [1]
s(X) → n__s(X) [1]
x(X1, X2) → n__x(X1, X2) [1]
activate(n__0) → 0' [1]
activate(n__plus(X1, X2)) → plus(X1, X2) [1]
activate(n__s(X)) → s(X) [1]
activate(n__x(X1, X2)) → x(X1, X2) [1]
activate(X) → X [1]
plus(N, 0') → U71(isNat(N), N) [1]
plus(N, s(M)) → U81(isNat(M), M, N) [1]
x(N, 0') → U91(isNat(N), N) [1]
x(N, s(M)) → U101(isNat(M), M, N) [1]
0' → n__0 [1]
s(X) → n__s(X) [1]
U101(tt, M, N) → U102(isNatKind(activate(M)), activate(M), activate(N)) [1]
U102(tt, M, N) → U103(isNat(activate(N)), activate(M), activate(N)) [1]
U103(tt, M, N) → U104(isNatKind(activate(N)), activate(M), activate(N)) [1]
U104(tt, M, N) → plus(x(activate(N), activate(M)), activate(N)) [1]
U11(tt, V1, V2) → U12(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
U12(tt, V1, V2) → U13(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U13(tt, V1, V2) → U14(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U14(tt, V1, V2) → U15(isNat(activate(V1)), activate(V2)) [1]
U15(tt, V2) → U16(isNat(activate(V2))) [1]
U16(tt) → tt [1]
U21(tt, V1) → U22(isNatKind(activate(V1)), activate(V1)) [1]
U22(tt, V1) → U23(isNat(activate(V1))) [1]
U23(tt) → tt [1]
U31(tt, V1, V2) → U32(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
U32(tt, V1, V2) → U33(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U33(tt, V1, V2) → U34(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U34(tt, V1, V2) → U35(isNat(activate(V1)), activate(V2)) [1]
U35(tt, V2) → U36(isNat(activate(V2))) [1]
U36(tt) → tt [1]
U41(tt, V2) → U42(isNatKind(activate(V2))) [1]
U42(tt) → tt [1]
U51(tt) → tt [1]
U61(tt, V2) → U62(isNatKind(activate(V2))) [1]
U62(tt) → tt [1]
U71(tt, N) → U72(isNatKind(activate(N)), activate(N)) [1]
U72(tt, N) → activate(N) [1]
U81(tt, M, N) → U82(isNatKind(activate(M)), activate(M), activate(N)) [1]
U82(tt, M, N) → U83(isNat(activate(N)), activate(M), activate(N)) [1]
U83(tt, M, N) → U84(isNatKind(activate(N)), activate(M), activate(N)) [1]
U84(tt, M, N) → s(plus(activate(N), activate(M))) [1]
U91(tt, N) → U92(isNatKind(activate(N))) [1]
U92(tt) → 0' [1]
isNat(n__0) → tt [1]
isNat(n__plus(V1, V2)) → U11(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
isNat(n__s(V1)) → U21(isNatKind(activate(V1)), activate(V1)) [1]
isNat(n__x(V1, V2)) → U31(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
isNatKind(n__0) → tt [1]
isNatKind(n__plus(V1, V2)) → U41(isNatKind(activate(V1)), activate(V2)) [1]
isNatKind(n__s(V1)) → U51(isNatKind(activate(V1))) [1]
isNatKind(n__x(V1, V2)) → U61(isNatKind(activate(V1)), activate(V2)) [1]
0' → n__0 [1]
plus(X1, X2) → n__plus(X1, X2) [1]
s(X) → n__s(X) [1]
x(X1, X2) → n__x(X1, X2) [1]
activate(n__0) → 0' [1]
activate(n__plus(X1, X2)) → plus(X1, X2) [1]
activate(n__s(X)) → s(X) [1]
activate(n__x(X1, X2)) → x(X1, X2) [1]
activate(X) → X [1]
U101(tt, M, N) → U102(isNatKind(activate(M)), activate(M), activate(N)) [1]
U102(tt, M, N) → U103(isNat(activate(N)), activate(M), activate(N)) [1]
U103(tt, M, N) → U104(isNatKind(activate(N)), activate(M), activate(N)) [1]
U104(tt, M, N) → plus(x(activate(N), activate(M)), activate(N)) [1]
U11(tt, V1, V2) → U12(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
U12(tt, V1, V2) → U13(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U13(tt, V1, V2) → U14(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U14(tt, V1, V2) → U15(isNat(activate(V1)), activate(V2)) [1]
U15(tt, V2) → U16(isNat(activate(V2))) [1]
U16(tt) → tt [1]
U21(tt, V1) → U22(isNatKind(activate(V1)), activate(V1)) [1]
U22(tt, V1) → U23(isNat(activate(V1))) [1]
U23(tt) → tt [1]
U31(tt, V1, V2) → U32(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
U32(tt, V1, V2) → U33(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U33(tt, V1, V2) → U34(isNatKind(activate(V2)), activate(V1), activate(V2)) [1]
U34(tt, V1, V2) → U35(isNat(activate(V1)), activate(V2)) [1]
U35(tt, V2) → U36(isNat(activate(V2))) [1]
U36(tt) → tt [1]
U41(tt, V2) → U42(isNatKind(activate(V2))) [1]
U42(tt) → tt [1]
U51(tt) → tt [1]
U61(tt, V2) → U62(isNatKind(activate(V2))) [1]
U62(tt) → tt [1]
U71(tt, N) → U72(isNatKind(activate(N)), activate(N)) [1]
U72(tt, N) → activate(N) [1]
U81(tt, M, N) → U82(isNatKind(activate(M)), activate(M), activate(N)) [1]
U82(tt, M, N) → U83(isNat(activate(N)), activate(M), activate(N)) [1]
U83(tt, M, N) → U84(isNatKind(activate(N)), activate(M), activate(N)) [1]
U84(tt, M, N) → s(plus(activate(N), activate(M))) [1]
U91(tt, N) → U92(isNatKind(activate(N))) [1]
U92(tt) → 0' [1]
isNat(n__0) → tt [1]
isNat(n__plus(V1, V2)) → U11(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
isNat(n__s(V1)) → U21(isNatKind(activate(V1)), activate(V1)) [1]
isNat(n__x(V1, V2)) → U31(isNatKind(activate(V1)), activate(V1), activate(V2)) [1]
isNatKind(n__0) → tt [1]
isNatKind(n__plus(V1, V2)) → U41(isNatKind(activate(V1)), activate(V2)) [1]
isNatKind(n__s(V1)) → U51(isNatKind(activate(V1))) [1]
isNatKind(n__x(V1, V2)) → U61(isNatKind(activate(V1)), activate(V2)) [1]
0' → n__0 [1]
plus(X1, X2) → n__plus(X1, X2) [1]
s(X) → n__s(X) [1]
x(X1, X2) → n__x(X1, X2) [1]
activate(n__0) → 0' [1]
activate(n__plus(X1, X2)) → plus(X1, X2) [1]
activate(n__s(X)) → s(X) [1]
activate(n__x(X1, X2)) → x(X1, X2) [1]
activate(X) → X [1]
| U101 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x tt :: tt U102 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x isNatKind :: n__0:n__plus:n__s:n__x → tt activate :: n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x U103 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x isNat :: n__0:n__plus:n__s:n__x → tt U104 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x plus :: n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x x :: n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x U11 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → tt U12 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → tt U13 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → tt U14 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → tt U15 :: tt → n__0:n__plus:n__s:n__x → tt U16 :: tt → tt U21 :: tt → n__0:n__plus:n__s:n__x → tt U22 :: tt → n__0:n__plus:n__s:n__x → tt U23 :: tt → tt U31 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → tt U32 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → tt U33 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → tt U34 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → tt U35 :: tt → n__0:n__plus:n__s:n__x → tt U36 :: tt → tt U41 :: tt → n__0:n__plus:n__s:n__x → tt U42 :: tt → tt U51 :: tt → tt U61 :: tt → n__0:n__plus:n__s:n__x → tt U62 :: tt → tt U71 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x U72 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x U81 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x U82 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x U83 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x U84 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x s :: n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x U91 :: tt → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x U92 :: tt → n__0:n__plus:n__s:n__x 0' :: n__0:n__plus:n__s:n__x n__0 :: n__0:n__plus:n__s:n__x n__plus :: n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x n__s :: n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x n__x :: n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x → n__0:n__plus:n__s:n__x |
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
tt => 0
n__0 => 0
0' -{ 1 }→ 0 :|:
U101(z, z', z'') -{ 1 }→ U102(isNatKind(activate(M)), activate(M), activate(N)) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U102(z, z', z'') -{ 1 }→ U103(isNat(activate(N)), activate(M), activate(N)) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U103(z, z', z'') -{ 1 }→ U104(isNatKind(activate(N)), activate(M), activate(N)) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U104(z, z', z'') -{ 1 }→ plus(x(activate(N), activate(M)), activate(N)) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U11(z, z', z'') -{ 1 }→ U12(isNatKind(activate(V1)), activate(V1), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 0, z'' = V2, z' = V1
U12(z, z', z'') -{ 1 }→ U13(isNatKind(activate(V2)), activate(V1), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 0, z'' = V2, z' = V1
U13(z, z', z'') -{ 1 }→ U14(isNatKind(activate(V2)), activate(V1), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 0, z'' = V2, z' = V1
U14(z, z', z'') -{ 1 }→ U15(isNat(activate(V1)), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 0, z'' = V2, z' = V1
U15(z, z') -{ 1 }→ U16(isNat(activate(V2))) :|: z' = V2, V2 >= 0, z = 0
U16(z) -{ 1 }→ 0 :|: z = 0
U21(z, z') -{ 1 }→ U22(isNatKind(activate(V1)), activate(V1)) :|: V1 >= 0, z = 0, z' = V1
U22(z, z') -{ 1 }→ U23(isNat(activate(V1))) :|: V1 >= 0, z = 0, z' = V1
U23(z) -{ 1 }→ 0 :|: z = 0
U31(z, z', z'') -{ 1 }→ U32(isNatKind(activate(V1)), activate(V1), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 0, z'' = V2, z' = V1
U32(z, z', z'') -{ 1 }→ U33(isNatKind(activate(V2)), activate(V1), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 0, z'' = V2, z' = V1
U33(z, z', z'') -{ 1 }→ U34(isNatKind(activate(V2)), activate(V1), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 0, z'' = V2, z' = V1
U34(z, z', z'') -{ 1 }→ U35(isNat(activate(V1)), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 0, z'' = V2, z' = V1
U35(z, z') -{ 1 }→ U36(isNat(activate(V2))) :|: z' = V2, V2 >= 0, z = 0
U36(z) -{ 1 }→ 0 :|: z = 0
U41(z, z') -{ 1 }→ U42(isNatKind(activate(V2))) :|: z' = V2, V2 >= 0, z = 0
U42(z) -{ 1 }→ 0 :|: z = 0
U51(z) -{ 1 }→ 0 :|: z = 0
U61(z, z') -{ 1 }→ U62(isNatKind(activate(V2))) :|: z' = V2, V2 >= 0, z = 0
U62(z) -{ 1 }→ 0 :|: z = 0
U71(z, z') -{ 1 }→ U72(isNatKind(activate(N)), activate(N)) :|: z' = N, z = 0, N >= 0
U72(z, z') -{ 1 }→ activate(N) :|: z' = N, z = 0, N >= 0
U81(z, z', z'') -{ 1 }→ U82(isNatKind(activate(M)), activate(M), activate(N)) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U82(z, z', z'') -{ 1 }→ U83(isNat(activate(N)), activate(M), activate(N)) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U83(z, z', z'') -{ 1 }→ U84(isNatKind(activate(N)), activate(M), activate(N)) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U84(z, z', z'') -{ 1 }→ s(plus(activate(N), activate(M))) :|: z' = M, z = 0, z'' = N, M >= 0, N >= 0
U91(z, z') -{ 1 }→ U92(isNatKind(activate(N))) :|: z' = N, z = 0, N >= 0
U92(z) -{ 1 }→ 0' :|: z = 0
activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 1 }→ x(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ s(X) :|: z = 1 + X, X >= 0
activate(z) -{ 1 }→ plus(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
activate(z) -{ 1 }→ 0' :|: z = 0
isNat(z) -{ 1 }→ U31(isNatKind(activate(V1)), activate(V1), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 1 + V1 + V2
isNat(z) -{ 1 }→ U21(isNatKind(activate(V1)), activate(V1)) :|: z = 1 + V1, V1 >= 0
isNat(z) -{ 1 }→ U11(isNatKind(activate(V1)), activate(V1), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 1 + V1 + V2
isNat(z) -{ 1 }→ 0 :|: z = 0
isNatKind(z) -{ 1 }→ U61(isNatKind(activate(V1)), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 1 + V1 + V2
isNatKind(z) -{ 1 }→ U51(isNatKind(activate(V1))) :|: z = 1 + V1, V1 >= 0
isNatKind(z) -{ 1 }→ U41(isNatKind(activate(V1)), activate(V2)) :|: V1 >= 0, V2 >= 0, z = 1 + V1 + V2
isNatKind(z) -{ 1 }→ 0 :|: z = 0
plus(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
s(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
x(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
| eq(start(V, V3, V4),0,[fun(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun1(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun2(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun3(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun4(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun5(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun6(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun7(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun8(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun9(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[fun10(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun11(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun12(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[fun13(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun14(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun15(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun16(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun17(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun18(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[fun19(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun20(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[fun21(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[fun22(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun23(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[fun24(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun25(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun26(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun27(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun28(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun29(V, V3, V4, Out)],[V >= 0,V3 >= 0,V4 >= 0]). eq(start(V, V3, V4),0,[fun30(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[fun31(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[isNat(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[isNatKind(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[fun32(Out)],[]). eq(start(V, V3, V4),0,[plus(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[s(V, Out)],[V >= 0]). eq(start(V, V3, V4),0,[x(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4),0,[activate(V, Out)],[V >= 0]). eq(fun(V, V3, V4, Out),1,[activate(M1, Ret00),isNatKind(Ret00, Ret0),activate(M1, Ret1),activate(N1, Ret2),fun1(Ret0, Ret1, Ret2, Ret)],[Out = Ret,V3 = M1,V = 0,V4 = N1,M1 >= 0,N1 >= 0]). eq(fun1(V, V3, V4, Out),1,[activate(N2, Ret001),isNat(Ret001, Ret01),activate(M2, Ret11),activate(N2, Ret21),fun2(Ret01, Ret11, Ret21, Ret3)],[Out = Ret3,V3 = M2,V = 0,V4 = N2,M2 >= 0,N2 >= 0]). eq(fun2(V, V3, V4, Out),1,[activate(N3, Ret002),isNatKind(Ret002, Ret02),activate(M3, Ret12),activate(N3, Ret22),fun3(Ret02, Ret12, Ret22, Ret4)],[Out = Ret4,V3 = M3,V = 0,V4 = N3,M3 >= 0,N3 >= 0]). eq(fun3(V, V3, V4, Out),1,[activate(N4, Ret003),activate(M4, Ret011),x(Ret003, Ret011, Ret03),activate(N4, Ret13),plus(Ret03, Ret13, Ret5)],[Out = Ret5,V3 = M4,V = 0,V4 = N4,M4 >= 0,N4 >= 0]). eq(fun4(V, V3, V4, Out),1,[activate(V11, Ret004),isNatKind(Ret004, Ret04),activate(V11, Ret14),activate(V21, Ret23),fun5(Ret04, Ret14, Ret23, Ret6)],[Out = Ret6,V11 >= 0,V21 >= 0,V = 0,V4 = V21,V3 = V11]). eq(fun5(V, V3, V4, Out),1,[activate(V22, Ret005),isNatKind(Ret005, Ret05),activate(V12, Ret15),activate(V22, Ret24),fun6(Ret05, Ret15, Ret24, Ret7)],[Out = Ret7,V12 >= 0,V22 >= 0,V = 0,V4 = V22,V3 = V12]). eq(fun6(V, V3, V4, Out),1,[activate(V23, Ret006),isNatKind(Ret006, Ret06),activate(V13, Ret16),activate(V23, Ret25),fun7(Ret06, Ret16, Ret25, Ret8)],[Out = Ret8,V13 >= 0,V23 >= 0,V = 0,V4 = V23,V3 = V13]). eq(fun7(V, V3, V4, Out),1,[activate(V14, Ret007),isNat(Ret007, Ret07),activate(V24, Ret17),fun8(Ret07, Ret17, Ret9)],[Out = Ret9,V14 >= 0,V24 >= 0,V = 0,V4 = V24,V3 = V14]). eq(fun8(V, V3, Out),1,[activate(V25, Ret008),isNat(Ret008, Ret08),fun9(Ret08, Ret10)],[Out = Ret10,V3 = V25,V25 >= 0,V = 0]). eq(fun9(V, Out),1,[],[Out = 0,V = 0]). eq(fun10(V, V3, Out),1,[activate(V15, Ret009),isNatKind(Ret009, Ret09),activate(V15, Ret18),fun11(Ret09, Ret18, Ret19)],[Out = Ret19,V15 >= 0,V = 0,V3 = V15]). eq(fun11(V, V3, Out),1,[activate(V16, Ret0010),isNat(Ret0010, Ret010),fun12(Ret010, Ret20)],[Out = Ret20,V16 >= 0,V = 0,V3 = V16]). eq(fun12(V, Out),1,[],[Out = 0,V = 0]). eq(fun13(V, V3, V4, Out),1,[activate(V17, Ret0011),isNatKind(Ret0011, Ret012),activate(V17, Ret110),activate(V26, Ret26),fun14(Ret012, Ret110, Ret26, Ret27)],[Out = Ret27,V17 >= 0,V26 >= 0,V = 0,V4 = V26,V3 = V17]). eq(fun14(V, V3, V4, Out),1,[activate(V27, Ret0012),isNatKind(Ret0012, Ret013),activate(V18, Ret111),activate(V27, Ret28),fun15(Ret013, Ret111, Ret28, Ret29)],[Out = Ret29,V18 >= 0,V27 >= 0,V = 0,V4 = V27,V3 = V18]). eq(fun15(V, V3, V4, Out),1,[activate(V28, Ret0013),isNatKind(Ret0013, Ret014),activate(V19, Ret112),activate(V28, Ret210),fun16(Ret014, Ret112, Ret210, Ret30)],[Out = Ret30,V19 >= 0,V28 >= 0,V = 0,V4 = V28,V3 = V19]). eq(fun16(V, V3, V4, Out),1,[activate(V110, Ret0014),isNat(Ret0014, Ret015),activate(V29, Ret113),fun17(Ret015, Ret113, Ret31)],[Out = Ret31,V110 >= 0,V29 >= 0,V = 0,V4 = V29,V3 = V110]). eq(fun17(V, V3, Out),1,[activate(V210, Ret0015),isNat(Ret0015, Ret016),fun18(Ret016, Ret32)],[Out = Ret32,V3 = V210,V210 >= 0,V = 0]). eq(fun18(V, Out),1,[],[Out = 0,V = 0]). eq(fun19(V, V3, Out),1,[activate(V211, Ret0016),isNatKind(Ret0016, Ret017),fun20(Ret017, Ret33)],[Out = Ret33,V3 = V211,V211 >= 0,V = 0]). eq(fun20(V, Out),1,[],[Out = 0,V = 0]). eq(fun21(V, Out),1,[],[Out = 0,V = 0]). eq(fun22(V, V3, Out),1,[activate(V212, Ret0017),isNatKind(Ret0017, Ret018),fun23(Ret018, Ret34)],[Out = Ret34,V3 = V212,V212 >= 0,V = 0]). eq(fun23(V, Out),1,[],[Out = 0,V = 0]). eq(fun24(V, V3, Out),1,[activate(N5, Ret0018),isNatKind(Ret0018, Ret019),activate(N5, Ret114),fun25(Ret019, Ret114, Ret35)],[Out = Ret35,V3 = N5,V = 0,N5 >= 0]). eq(fun25(V, V3, Out),1,[activate(N6, Ret36)],[Out = Ret36,V3 = N6,V = 0,N6 >= 0]). eq(fun26(V, V3, V4, Out),1,[activate(M5, Ret0019),isNatKind(Ret0019, Ret020),activate(M5, Ret115),activate(N7, Ret211),fun27(Ret020, Ret115, Ret211, Ret37)],[Out = Ret37,V3 = M5,V = 0,V4 = N7,M5 >= 0,N7 >= 0]). eq(fun27(V, V3, V4, Out),1,[activate(N8, Ret0020),isNat(Ret0020, Ret021),activate(M6, Ret116),activate(N8, Ret212),fun28(Ret021, Ret116, Ret212, Ret38)],[Out = Ret38,V3 = M6,V = 0,V4 = N8,M6 >= 0,N8 >= 0]). eq(fun28(V, V3, V4, Out),1,[activate(N9, Ret0021),isNatKind(Ret0021, Ret022),activate(M7, Ret117),activate(N9, Ret213),fun29(Ret022, Ret117, Ret213, Ret39)],[Out = Ret39,V3 = M7,V = 0,V4 = N9,M7 >= 0,N9 >= 0]). eq(fun29(V, V3, V4, Out),1,[activate(N10, Ret0022),activate(M8, Ret0110),plus(Ret0022, Ret0110, Ret023),s(Ret023, Ret40)],[Out = Ret40,V3 = M8,V = 0,V4 = N10,M8 >= 0,N10 >= 0]). eq(fun30(V, V3, Out),1,[activate(N11, Ret0023),isNatKind(Ret0023, Ret024),fun31(Ret024, Ret41)],[Out = Ret41,V3 = N11,V = 0,N11 >= 0]). eq(fun31(V, Out),1,[fun32(Ret42)],[Out = Ret42,V = 0]). eq(isNat(V, Out),1,[],[Out = 0,V = 0]). eq(isNat(V, Out),1,[activate(V111, Ret0024),isNatKind(Ret0024, Ret025),activate(V111, Ret118),activate(V213, Ret214),fun4(Ret025, Ret118, Ret214, Ret43)],[Out = Ret43,V111 >= 0,V213 >= 0,V = 1 + V111 + V213]). eq(isNat(V, Out),1,[activate(V112, Ret0025),isNatKind(Ret0025, Ret026),activate(V112, Ret119),fun10(Ret026, Ret119, Ret44)],[Out = Ret44,V = 1 + V112,V112 >= 0]). eq(isNat(V, Out),1,[activate(V113, Ret0026),isNatKind(Ret0026, Ret027),activate(V113, Ret120),activate(V214, Ret215),fun13(Ret027, Ret120, Ret215, Ret45)],[Out = Ret45,V113 >= 0,V214 >= 0,V = 1 + V113 + V214]). eq(isNatKind(V, Out),1,[],[Out = 0,V = 0]). eq(isNatKind(V, Out),1,[activate(V114, Ret0027),isNatKind(Ret0027, Ret028),activate(V215, Ret121),fun19(Ret028, Ret121, Ret46)],[Out = Ret46,V114 >= 0,V215 >= 0,V = 1 + V114 + V215]). eq(isNatKind(V, Out),1,[activate(V115, Ret0028),isNatKind(Ret0028, Ret029),fun21(Ret029, Ret47)],[Out = Ret47,V = 1 + V115,V115 >= 0]). eq(isNatKind(V, Out),1,[activate(V116, Ret0029),isNatKind(Ret0029, Ret030),activate(V216, Ret122),fun22(Ret030, Ret122, Ret48)],[Out = Ret48,V116 >= 0,V216 >= 0,V = 1 + V116 + V216]). eq(fun32(Out),1,[],[Out = 0]). eq(plus(V, V3, Out),1,[],[Out = 1 + X11 + X21,X11 >= 0,X21 >= 0,V = X11,V3 = X21]). eq(s(V, Out),1,[],[Out = 1 + X3,X3 >= 0,V = X3]). eq(x(V, V3, Out),1,[],[Out = 1 + X12 + X22,X12 >= 0,X22 >= 0,V = X12,V3 = X22]). eq(activate(V, Out),1,[fun32(Ret49)],[Out = Ret49,V = 0]). eq(activate(V, Out),1,[plus(X13, X23, Ret50)],[Out = Ret50,X13 >= 0,X23 >= 0,V = 1 + X13 + X23]). eq(activate(V, Out),1,[s(X4, Ret51)],[Out = Ret51,V = 1 + X4,X4 >= 0]). eq(activate(V, Out),1,[x(X14, X24, Ret52)],[Out = Ret52,X14 >= 0,X24 >= 0,V = 1 + X14 + X24]). eq(activate(V, Out),1,[],[Out = X5,X5 >= 0,V = X5]). input_output_vars(fun(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun1(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun2(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun3(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun4(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun5(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun6(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun7(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun8(V,V3,Out),[V,V3],[Out]). input_output_vars(fun9(V,Out),[V],[Out]). input_output_vars(fun10(V,V3,Out),[V,V3],[Out]). input_output_vars(fun11(V,V3,Out),[V,V3],[Out]). input_output_vars(fun12(V,Out),[V],[Out]). input_output_vars(fun13(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun14(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun15(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun16(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun17(V,V3,Out),[V,V3],[Out]). input_output_vars(fun18(V,Out),[V],[Out]). input_output_vars(fun19(V,V3,Out),[V,V3],[Out]). input_output_vars(fun20(V,Out),[V],[Out]). input_output_vars(fun21(V,Out),[V],[Out]). input_output_vars(fun22(V,V3,Out),[V,V3],[Out]). input_output_vars(fun23(V,Out),[V],[Out]). input_output_vars(fun24(V,V3,Out),[V,V3],[Out]). input_output_vars(fun25(V,V3,Out),[V,V3],[Out]). input_output_vars(fun26(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun27(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun28(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun29(V,V3,V4,Out),[V,V3,V4],[Out]). input_output_vars(fun30(V,V3,Out),[V,V3],[Out]). input_output_vars(fun31(V,Out),[V],[Out]). input_output_vars(isNat(V,Out),[V],[Out]). input_output_vars(isNatKind(V,Out),[V],[Out]). input_output_vars(fun32(Out),[],[Out]). input_output_vars(plus(V,V3,Out),[V,V3],[Out]). input_output_vars(s(V,Out),[V],[Out]). input_output_vars(x(V,V3,Out),[V,V3],[Out]). input_output_vars(activate(V,Out),[V],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. non_recursive : [fun32/1]
1. non_recursive : [plus/3]
2. non_recursive : [s/2]
3. non_recursive : [x/3]
4. non_recursive : [activate/2]
5. non_recursive : [fun3/4]
6. non_recursive : [fun20/2]
7. non_recursive : [fun21/2]
8. non_recursive : [fun23/2]
9. recursive [non_tail,multiple] : [fun19/3,fun22/3,isNatKind/2]
10. non_recursive : [fun2/4]
11. non_recursive : [fun12/2]
12. non_recursive : [fun18/2]
13. non_recursive : [fun9/2]
14. recursive [non_tail,multiple] : [fun10/3,fun11/3,fun13/4,fun14/4,fun15/4,fun16/4,fun17/3,fun4/4,fun5/4,fun6/4,fun7/4,fun8/3,isNat/2]
15. non_recursive : [fun1/4]
16. non_recursive : [fun/4]
17. non_recursive : [fun25/3]
18. non_recursive : [fun24/3]
19. non_recursive : [fun29/4]
20. non_recursive : [fun28/4]
21. non_recursive : [fun27/4]
22. non_recursive : [fun26/4]
23. non_recursive : [fun31/2]
24. non_recursive : [fun30/3]
25. non_recursive : [start/3]
#### Obtained direct recursion through partial evaluation
0. SCC is completely evaluated into other SCCs
1. SCC is completely evaluated into other SCCs
2. SCC is completely evaluated into other SCCs
3. SCC is completely evaluated into other SCCs
4. SCC is partially evaluated into activate/2
5. SCC is partially evaluated into fun3/4
6. SCC is completely evaluated into other SCCs
7. SCC is completely evaluated into other SCCs
8. SCC is completely evaluated into other SCCs
9. SCC is partially evaluated into isNatKind/2
10. SCC is partially evaluated into fun2/4
11. SCC is completely evaluated into other SCCs
12. SCC is completely evaluated into other SCCs
13. SCC is completely evaluated into other SCCs
14. SCC is partially evaluated into isNat/2
15. SCC is partially evaluated into fun1/4
16. SCC is partially evaluated into fun/4
17. SCC is completely evaluated into other SCCs
18. SCC is partially evaluated into fun24/3
19. SCC is partially evaluated into fun29/4
20. SCC is partially evaluated into fun28/4
21. SCC is partially evaluated into fun27/4
22. SCC is partially evaluated into fun26/4
23. SCC is completely evaluated into other SCCs
24. SCC is partially evaluated into fun30/3
25. SCC is partially evaluated into start/3
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations activate/2
* CE 25 is refined into CE [44]
* CE 26 is refined into CE [45]
* CE 27 is refined into CE [46]
### Cost equations --> "Loop" of activate/2
* CEs [44,45,46] --> Loop 19
### Ranking functions of CR activate(V,Out)
#### Partial ranking functions of CR activate(V,Out)
### Specialization of cost equations fun3/4
* CE 37 is refined into CE [47]
### Cost equations --> "Loop" of fun3/4
* CEs [47] --> Loop 20
### Ranking functions of CR fun3(V,V3,V4,Out)
#### Partial ranking functions of CR fun3(V,V3,V4,Out)
### Specialization of cost equations isNatKind/2
* CE 30 is refined into CE [48]
* CE 29 is refined into CE [49]
* CE 28 is refined into CE [50]
### Cost equations --> "Loop" of isNatKind/2
* CEs [50] --> Loop 21
* CEs [49] --> Loop 22
* CEs [48] --> Loop 23
### Ranking functions of CR isNatKind(V,Out)
* RF of phase [21,23]: [V]
#### Partial ranking functions of CR isNatKind(V,Out)
* Partial RF of phase [21,23]:
- RF of loop [21:1,21:2,23:1]:
V
### Specialization of cost equations fun2/4
* CE 36 is refined into CE [51,52]
### Cost equations --> "Loop" of fun2/4
* CEs [52] --> Loop 24
* CEs [51] --> Loop 25
### Ranking functions of CR fun2(V,V3,V4,Out)
#### Partial ranking functions of CR fun2(V,V3,V4,Out)
### Specialization of cost equations isNat/2
* CE 33 is refined into CE [53]
* CE 32 is refined into CE [54,55]
* CE 31 is refined into CE [56,57,58,59]
### Cost equations --> "Loop" of isNat/2
* CEs [59] --> Loop 26
* CEs [58] --> Loop 27
* CEs [57] --> Loop 28
* CEs [56] --> Loop 29
* CEs [55] --> Loop 30
* CEs [54] --> Loop 31
* CEs [53] --> Loop 32
### Ranking functions of CR isNat(V,Out)
* RF of phase [26,27,28,30]: [V-1]
#### Partial ranking functions of CR isNat(V,Out)
* Partial RF of phase [26,27,28,30]:
- RF of loop [26:1,26:2]:
V/2-1
- RF of loop [27:1,27:2,28:1,28:2,30:1]:
V-1
### Specialization of cost equations fun1/4
* CE 35 is refined into CE [60,61,62]
### Cost equations --> "Loop" of fun1/4
* CEs [62] --> Loop 33
* CEs [61] --> Loop 34
* CEs [60] --> Loop 35
### Ranking functions of CR fun1(V,V3,V4,Out)
#### Partial ranking functions of CR fun1(V,V3,V4,Out)
### Specialization of cost equations fun/4
* CE 34 is refined into CE [63,64,65,66,67,68]
### Cost equations --> "Loop" of fun/4
* CEs [68] --> Loop 36
* CEs [67] --> Loop 37
* CEs [66] --> Loop 38
* CEs [65] --> Loop 39
* CEs [64] --> Loop 40
* CEs [63] --> Loop 41
### Ranking functions of CR fun(V,V3,V4,Out)
#### Partial ranking functions of CR fun(V,V3,V4,Out)
### Specialization of cost equations fun24/3
* CE 38 is refined into CE [69,70]
### Cost equations --> "Loop" of fun24/3
* CEs [70] --> Loop 42
* CEs [69] --> Loop 43
### Ranking functions of CR fun24(V,V3,Out)
#### Partial ranking functions of CR fun24(V,V3,Out)
### Specialization of cost equations fun29/4
* CE 42 is refined into CE [71]
### Cost equations --> "Loop" of fun29/4
* CEs [71] --> Loop 44
### Ranking functions of CR fun29(V,V3,V4,Out)
#### Partial ranking functions of CR fun29(V,V3,V4,Out)
### Specialization of cost equations fun28/4
* CE 41 is refined into CE [72,73]
### Cost equations --> "Loop" of fun28/4
* CEs [73] --> Loop 45
* CEs [72] --> Loop 46
### Ranking functions of CR fun28(V,V3,V4,Out)
#### Partial ranking functions of CR fun28(V,V3,V4,Out)
### Specialization of cost equations fun27/4
* CE 40 is refined into CE [74,75,76]
### Cost equations --> "Loop" of fun27/4
* CEs [76] --> Loop 47
* CEs [75] --> Loop 48
* CEs [74] --> Loop 49
### Ranking functions of CR fun27(V,V3,V4,Out)
#### Partial ranking functions of CR fun27(V,V3,V4,Out)
### Specialization of cost equations fun26/4
* CE 39 is refined into CE [77,78,79,80,81,82]
### Cost equations --> "Loop" of fun26/4
* CEs [82] --> Loop 50
* CEs [81] --> Loop 51
* CEs [80] --> Loop 52
* CEs [79] --> Loop 53
* CEs [78] --> Loop 54
* CEs [77] --> Loop 55
### Ranking functions of CR fun26(V,V3,V4,Out)
#### Partial ranking functions of CR fun26(V,V3,V4,Out)
### Specialization of cost equations fun30/3
* CE 43 is refined into CE [83,84]
### Cost equations --> "Loop" of fun30/3
* CEs [84] --> Loop 56
* CEs [83] --> Loop 57
### Ranking functions of CR fun30(V,V3,Out)
#### Partial ranking functions of CR fun30(V,V3,Out)
### Specialization of cost equations start/3
* CE 2 is refined into CE [85,86,87,88,89,90,91,92,93]
* CE 3 is refined into CE [94,95,96,97,98,99,100,101,102]
* CE 4 is refined into CE [103,104,105,106,107,108,109,110,111]
* CE 5 is refined into CE [112,113,114,115,116,117,118,119,120]
* CE 6 is refined into CE [121,122,123]
* CE 7 is refined into CE [124,125,126]
* CE 8 is refined into CE [127,128]
* CE 9 is refined into CE [129,130,131,132,133,134]
* CE 10 is refined into CE [135,136,137]
* CE 11 is refined into CE [138,139]
* CE 12 is refined into CE [140]
* CE 13 is refined into CE [141]
* CE 14 is refined into CE [142,143]
* CE 15 is refined into CE [144]
* CE 16 is refined into CE [145,146,147,148,149,150]
* CE 17 is refined into CE [151,152,153]
* CE 18 is refined into CE [154,155]
* CE 19 is refined into CE [156]
* CE 20 is refined into CE [157,158]
* CE 21 is refined into CE [159]
* CE 22 is refined into CE [160,161,162]
* CE 23 is refined into CE [163,164]
* CE 24 is refined into CE [165]
### Cost equations --> "Loop" of start/3
* CEs [85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165] --> Loop 58
### Ranking functions of CR start(V,V3,V4)
#### Partial ranking functions of CR start(V,V3,V4)
Computing Bounds
=====================================
#### Cost of chains of activate(V,Out):
* Chain [19]: 2
with precondition: [V=Out,V>=0]
#### Cost of chains of fun3(V,V3,V4,Out):
* Chain [20]: 9
with precondition: [V=0,V3+2*V4+2=Out,V3>=0,V4>=0]
#### Cost of chains of isNatKind(V,Out):
* Chain [22]: 1
with precondition: [V=0,Out=0]
* Chain [multiple([21,23],[[22]])]: 13*it(21)+1*it([22])+0
Such that:it([22]) =< V+1
aux(1) =< V
it(21) =< aux(1)
with precondition: [Out=0,V>=1]
#### Cost of chains of fun2(V,V3,V4,Out):
* Chain [25]: 17
with precondition: [V=0,V4=0,V3+2=Out,V3>=0]
* Chain [24]: 1*s(1)+13*s(3)+16
Such that:s(2) =< V4
s(1) =< V4+1
s(3) =< s(2)
with precondition: [V=0,V3+2*V4+2=Out,V3>=0,V4>=1]
#### Cost of chains of isNat(V,Out):
* Chain [32]: 1
with precondition: [V=0,Out=0]
* Chain [31,32]: 17
with precondition: [V=1,Out=0]
* Chain [multiple(29,[[32]])]: 43
with precondition: [V=1,Out=0]
* Chain [multiple([26,27,28,30],[[32],[31,32],[multiple(29,[[32]])]])]: 37*it(26)+78*it(27)+14*it(30)+17*it([31,32])+1*it([32])+43*it([multiple(29,[[32]])])+28*s(52)+2*s(53)+26*s(54)+4*s(58)+52*s(59)+2*s(66)+26*s(67)+0
Such that:aux(25) =< V
aux(26) =< V+1
aux(27) =< V/2
aux(28) =< V/2+1/2
aux(29) =< 2/3*V
it(30) =< aux(25)
it([32]) =< aux(26)
it([multiple(29,[[32]])]) =< aux(26)
it(26) =< aux(27)
it([31,32]) =< aux(28)
it([multiple(29,[[32]])]) =< aux(28)
it(27) =< aux(29)
aux(17) =< aux(25)+1
aux(14) =< aux(25)
aux(13) =< aux(25)-1
it(30) =< it([32])+aux(25)
it(27) =< it([32])* (1/3)+aux(29)
it(26) =< it([32])* (1/2)+aux(27)
it(27) =< it([32])* (1/2)+aux(27)
s(69) =< it(30)*aux(17)
s(68) =< it(30)*aux(14)
s(61) =< it(27)*aux(17)
s(60) =< it(27)*aux(14)
s(56) =< it(26)*aux(14)
s(55) =< it(26)*aux(13)
s(57) =< it(26)*aux(25)
s(66) =< s(69)
s(67) =< s(68)
s(58) =< s(61)
s(59) =< s(60)
s(52) =< s(57)
s(53) =< s(56)
s(54) =< s(55)
with precondition: [Out=0,V>=2]
#### Cost of chains of fun1(V,V3,V4,Out):
* Chain [35]: 25
with precondition: [V=0,V4=0,V3+2=Out,V3>=0]
* Chain [34]: 1*s(71)+13*s(72)+66
Such that:s(70) =< 1
s(71) =< 2
s(72) =< s(70)
with precondition: [V=0,V4=1,V3+4=Out,V3>=0]
* Chain [33]: 14*s(78)+2*s(79)+43*s(80)+37*s(81)+17*s(82)+78*s(83)+2*s(94)+26*s(95)+4*s(96)+52*s(97)+28*s(98)+2*s(99)+26*s(100)+13*s(103)+23
Such that:s(75) =< V4/2
s(76) =< V4/2+1/2
s(77) =< 2/3*V4
aux(30) =< V4
aux(31) =< V4+1
s(79) =< aux(31)
s(103) =< aux(30)
s(78) =< aux(30)
s(80) =< aux(31)
s(81) =< s(75)
s(82) =< s(76)
s(80) =< s(76)
s(83) =< s(77)
s(84) =< aux(30)+1
s(85) =< aux(30)
s(86) =< aux(30)-1
s(78) =< s(79)+aux(30)
s(83) =< s(79)* (1/3)+s(77)
s(81) =< s(79)* (1/2)+s(75)
s(83) =< s(79)* (1/2)+s(75)
s(87) =< s(78)*s(84)
s(88) =< s(78)*s(85)
s(89) =< s(83)*s(84)
s(90) =< s(83)*s(85)
s(91) =< s(81)*s(85)
s(92) =< s(81)*s(86)
s(93) =< s(81)*aux(30)
s(94) =< s(87)
s(95) =< s(88)
s(96) =< s(89)
s(97) =< s(90)
s(98) =< s(93)
s(99) =< s(91)
s(100) =< s(92)
with precondition: [V=0,V3+2*V4+2=Out,V3>=0,V4>=2]
#### Cost of chains of fun(V,V3,V4,Out):
* Chain [41]: 33
with precondition: [V=0,V3=0,V4=0,Out=2]
* Chain [40]: 1*s(105)+13*s(106)+74
Such that:s(104) =< 1
s(105) =< 2
s(106) =< s(104)
with precondition: [V=0,V3=0,V4=1,Out=4]
* Chain [39]: 2*s(112)+13*s(113)+14*s(114)+43*s(115)+37*s(116)+17*s(117)+78*s(118)+2*s(129)+26*s(130)+4*s(131)+52*s(132)+28*s(133)+2*s(134)+26*s(135)+31
Such that:s(110) =< V4
s(111) =< V4+1
s(107) =< V4/2
s(108) =< V4/2+1/2
s(109) =< 2/3*V4
s(112) =< s(111)
s(113) =< s(110)
s(114) =< s(110)
s(115) =< s(111)
s(116) =< s(107)
s(117) =< s(108)
s(115) =< s(108)
s(118) =< s(109)
s(119) =< s(110)+1
s(120) =< s(110)
s(121) =< s(110)-1
s(114) =< s(112)+s(110)
s(118) =< s(112)* (1/3)+s(109)
s(116) =< s(112)* (1/2)+s(107)
s(118) =< s(112)* (1/2)+s(107)
s(122) =< s(114)*s(119)
s(123) =< s(114)*s(120)
s(124) =< s(118)*s(119)
s(125) =< s(118)*s(120)
s(126) =< s(116)*s(120)
s(127) =< s(116)*s(121)
s(128) =< s(116)*s(110)
s(129) =< s(122)
s(130) =< s(123)
s(131) =< s(124)
s(132) =< s(125)
s(133) =< s(128)
s(134) =< s(126)
s(135) =< s(127)
with precondition: [V=0,V3=0,2*V4+2=Out,V4>=2]
* Chain [38]: 1*s(136)+13*s(138)+32
Such that:s(137) =< V3
s(136) =< V3+1
s(138) =< s(137)
with precondition: [V=0,V4=0,V3+2=Out,V3>=1]
* Chain [37]: 1*s(139)+13*s(141)+1*s(143)+13*s(144)+73
Such that:s(142) =< 1
s(143) =< 2
s(140) =< V3
s(139) =< V3+1
s(144) =< s(142)
s(141) =< s(140)
with precondition: [V=0,V4=1,V3+4=Out,V3>=1]
* Chain [36]: 1*s(145)+13*s(147)+2*s(153)+13*s(154)+14*s(155)+43*s(156)+37*s(157)+17*s(158)+78*s(159)+2*s(170)+26*s(171)+4*s(172)+52*s(173)+28*s(174)+2*s(175)+26*s(176)+30
Such that:s(146) =< V3
s(145) =< V3+1
s(151) =< V4
s(152) =< V4+1
s(148) =< V4/2
s(149) =< V4/2+1/2
s(150) =< 2/3*V4
s(153) =< s(152)
s(154) =< s(151)
s(155) =< s(151)
s(156) =< s(152)
s(157) =< s(148)
s(158) =< s(149)
s(156) =< s(149)
s(159) =< s(150)
s(160) =< s(151)+1
s(161) =< s(151)
s(162) =< s(151)-1
s(155) =< s(153)+s(151)
s(159) =< s(153)* (1/3)+s(150)
s(157) =< s(153)* (1/2)+s(148)
s(159) =< s(153)* (1/2)+s(148)
s(163) =< s(155)*s(160)
s(164) =< s(155)*s(161)
s(165) =< s(159)*s(160)
s(166) =< s(159)*s(161)
s(167) =< s(157)*s(161)
s(168) =< s(157)*s(162)
s(169) =< s(157)*s(151)
s(170) =< s(163)
s(171) =< s(164)
s(172) =< s(165)
s(173) =< s(166)
s(174) =< s(169)
s(175) =< s(167)
s(176) =< s(168)
s(147) =< s(146)
with precondition: [V=0,V3+2*V4+2=Out,V3>=1,V4>=2]
#### Cost of chains of fun24(V,V3,Out):
* Chain [43]: 9
with precondition: [V=0,V3=0,Out=0]
* Chain [42]: 1*s(177)+13*s(179)+8
Such that:s(178) =< V3
s(177) =< V3+1
s(179) =< s(178)
with precondition: [V=0,V3=Out,V3>=1]
#### Cost of chains of fun29(V,V3,V4,Out):
* Chain [44]: 7
with precondition: [V=0,V3+V4+2=Out,V3>=0,V4>=0]
#### Cost of chains of fun28(V,V3,V4,Out):
* Chain [46]: 15
with precondition: [V=0,V4=0,V3+2=Out,V3>=0]
* Chain [45]: 1*s(180)+13*s(182)+14
Such that:s(181) =< V4
s(180) =< V4+1
s(182) =< s(181)
with precondition: [V=0,V3+V4+2=Out,V3>=0,V4>=1]
#### Cost of chains of fun27(V,V3,V4,Out):
* Chain [49]: 23
with precondition: [V=0,V4=0,V3+2=Out,V3>=0]
* Chain [48]: 1*s(184)+13*s(185)+64
Such that:s(183) =< 1
s(184) =< 2
s(185) =< s(183)
with precondition: [V=0,V4=1,V3+3=Out,V3>=0]
* Chain [47]: 14*s(191)+2*s(192)+43*s(193)+37*s(194)+17*s(195)+78*s(196)+2*s(207)+26*s(208)+4*s(209)+52*s(210)+28*s(211)+2*s(212)+26*s(213)+13*s(216)+21
Such that:s(188) =< V4/2
s(189) =< V4/2+1/2
s(190) =< 2/3*V4
aux(32) =< V4
aux(33) =< V4+1
s(192) =< aux(33)
s(216) =< aux(32)
s(191) =< aux(32)
s(193) =< aux(33)
s(194) =< s(188)
s(195) =< s(189)
s(193) =< s(189)
s(196) =< s(190)
s(197) =< aux(32)+1
s(198) =< aux(32)
s(199) =< aux(32)-1
s(191) =< s(192)+aux(32)
s(196) =< s(192)* (1/3)+s(190)
s(194) =< s(192)* (1/2)+s(188)
s(196) =< s(192)* (1/2)+s(188)
s(200) =< s(191)*s(197)
s(201) =< s(191)*s(198)
s(202) =< s(196)*s(197)
s(203) =< s(196)*s(198)
s(204) =< s(194)*s(198)
s(205) =< s(194)*s(199)
s(206) =< s(194)*aux(32)
s(207) =< s(200)
s(208) =< s(201)
s(209) =< s(202)
s(210) =< s(203)
s(211) =< s(206)
s(212) =< s(204)
s(213) =< s(205)
with precondition: [V=0,V3+V4+2=Out,V3>=0,V4>=2]
#### Cost of chains of fun26(V,V3,V4,Out):
* Chain [55]: 31
with precondition: [V=0,V3=0,V4=0,Out=2]
* Chain [54]: 1*s(218)+13*s(219)+72
Such that:s(217) =< 1
s(218) =< 2
s(219) =< s(217)
with precondition: [V=0,V3=0,V4=1,Out=3]
* Chain [53]: 2*s(225)+13*s(226)+14*s(227)+43*s(228)+37*s(229)+17*s(230)+78*s(231)+2*s(242)+26*s(243)+4*s(244)+52*s(245)+28*s(246)+2*s(247)+26*s(248)+29
Such that:s(223) =< V4
s(224) =< V4+1
s(220) =< V4/2
s(221) =< V4/2+1/2
s(222) =< 2/3*V4
s(225) =< s(224)
s(226) =< s(223)
s(227) =< s(223)
s(228) =< s(224)
s(229) =< s(220)
s(230) =< s(221)
s(228) =< s(221)
s(231) =< s(222)
s(232) =< s(223)+1
s(233) =< s(223)
s(234) =< s(223)-1
s(227) =< s(225)+s(223)
s(231) =< s(225)* (1/3)+s(222)
s(229) =< s(225)* (1/2)+s(220)
s(231) =< s(225)* (1/2)+s(220)
s(235) =< s(227)*s(232)
s(236) =< s(227)*s(233)
s(237) =< s(231)*s(232)
s(238) =< s(231)*s(233)
s(239) =< s(229)*s(233)
s(240) =< s(229)*s(234)
s(241) =< s(229)*s(223)
s(242) =< s(235)
s(243) =< s(236)
s(244) =< s(237)
s(245) =< s(238)
s(246) =< s(241)
s(247) =< s(239)
s(248) =< s(240)
with precondition: [V=0,V3=0,V4+2=Out,V4>=2]
* Chain [52]: 1*s(249)+13*s(251)+30
Such that:s(250) =< V3
s(249) =< V3+1
s(251) =< s(250)
with precondition: [V=0,V4=0,V3+2=Out,V3>=1]
* Chain [51]: 1*s(252)+13*s(254)+1*s(256)+13*s(257)+71
Such that:s(255) =< 1
s(256) =< 2
s(253) =< V3
s(252) =< V3+1
s(257) =< s(255)
s(254) =< s(253)
with precondition: [V=0,V4=1,V3+3=Out,V3>=1]
* Chain [50]: 1*s(258)+13*s(260)+2*s(266)+13*s(267)+14*s(268)+43*s(269)+37*s(270)+17*s(271)+78*s(272)+2*s(283)+26*s(284)+4*s(285)+52*s(286)+28*s(287)+2*s(288)+26*s(289)+28
Such that:s(259) =< V3
s(258) =< V3+1
s(264) =< V4
s(265) =< V4+1
s(261) =< V4/2
s(262) =< V4/2+1/2
s(263) =< 2/3*V4
s(266) =< s(265)
s(267) =< s(264)
s(268) =< s(264)
s(269) =< s(265)
s(270) =< s(261)
s(271) =< s(262)
s(269) =< s(262)
s(272) =< s(263)
s(273) =< s(264)+1
s(274) =< s(264)
s(275) =< s(264)-1
s(268) =< s(266)+s(264)
s(272) =< s(266)* (1/3)+s(263)
s(270) =< s(266)* (1/2)+s(261)
s(272) =< s(266)* (1/2)+s(261)
s(276) =< s(268)*s(273)
s(277) =< s(268)*s(274)
s(278) =< s(272)*s(273)
s(279) =< s(272)*s(274)
s(280) =< s(270)*s(274)
s(281) =< s(270)*s(275)
s(282) =< s(270)*s(264)
s(283) =< s(276)
s(284) =< s(277)
s(285) =< s(278)
s(286) =< s(279)
s(287) =< s(282)
s(288) =< s(280)
s(289) =< s(281)
s(260) =< s(259)
with precondition: [V=0,V3+V4+2=Out,V3>=1,V4>=2]
#### Cost of chains of fun30(V,V3,Out):
* Chain [57]: 6
with precondition: [V=0,V3=0,Out=0]
* Chain [56]: 1*s(290)+13*s(292)+5
Such that:s(291) =< V3
s(290) =< V3+1
s(292) =< s(291)
with precondition: [V=0,Out=0,V3>=1]
#### Cost of chains of start(V,V3,V4):
* Chain [58]: 25*s(293)+325*s(295)+41*s(299)+299*s(301)+252*s(310)+774*s(312)+666*s(313)+306*s(314)+1404*s(315)+36*s(326)+468*s(327)+72*s(328)+936*s(329)+504*s(330)+36*s(331)+468*s(332)+27*s(336)+169*s(338)+196*s(344)+602*s(346)+518*s(347)+238*s(348)+1092*s(349)+28*s(360)+364*s(361)+56*s(362)+728*s(363)+392*s(364)+28*s(365)+364*s(366)+14*s(1365)+2*s(1366)+43*s(1367)+37*s(1368)+17*s(1369)+78*s(1370)+2*s(1381)+26*s(1382)+4*s(1383)+52*s(1384)+28*s(1385)+2*s(1386)+26*s(1387)+13*s(1390)+116
Such that:s(1362) =< V/2
s(1363) =< V/2+1/2
s(1364) =< 2/3*V
aux(72) =< 1
aux(73) =< 2
aux(74) =< V
aux(75) =< V+1
aux(76) =< V3
aux(77) =< V3+1
aux(78) =< V3/2
aux(79) =< V3/2+1/2
aux(80) =< 2/3*V3
aux(81) =< V4
aux(82) =< V4+1
aux(83) =< V4/2
aux(84) =< V4/2+1/2
aux(85) =< 2/3*V4
s(293) =< aux(73)
s(1366) =< aux(75)
s(336) =< aux(77)
s(299) =< aux(82)
s(295) =< aux(72)
s(310) =< aux(81)
s(312) =< aux(82)
s(313) =< aux(83)
s(314) =< aux(84)
s(312) =< aux(84)
s(315) =< aux(85)
s(316) =< aux(81)+1
s(317) =< aux(81)
s(318) =< aux(81)-1
s(310) =< s(299)+aux(81)
s(315) =< s(299)* (1/3)+aux(85)
s(313) =< s(299)* (1/2)+aux(83)
s(315) =< s(299)* (1/2)+aux(83)
s(319) =< s(310)*s(316)
s(320) =< s(310)*s(317)
s(321) =< s(315)*s(316)
s(322) =< s(315)*s(317)
s(323) =< s(313)*s(317)
s(324) =< s(313)*s(318)
s(325) =< s(313)*aux(81)
s(326) =< s(319)
s(327) =< s(320)
s(328) =< s(321)
s(329) =< s(322)
s(330) =< s(325)
s(331) =< s(323)
s(332) =< s(324)
s(301) =< aux(81)
s(344) =< aux(76)
s(346) =< aux(77)
s(347) =< aux(78)
s(348) =< aux(79)
s(346) =< aux(79)
s(349) =< aux(80)
s(350) =< aux(76)+1
s(351) =< aux(76)
s(352) =< aux(76)-1
s(344) =< s(336)+aux(76)
s(349) =< s(336)* (1/3)+aux(80)
s(347) =< s(336)* (1/2)+aux(78)
s(349) =< s(336)* (1/2)+aux(78)
s(353) =< s(344)*s(350)
s(354) =< s(344)*s(351)
s(355) =< s(349)*s(350)
s(356) =< s(349)*s(351)
s(357) =< s(347)*s(351)
s(358) =< s(347)*s(352)
s(359) =< s(347)*aux(76)
s(360) =< s(353)
s(361) =< s(354)
s(362) =< s(355)
s(363) =< s(356)
s(364) =< s(359)
s(365) =< s(357)
s(366) =< s(358)
s(338) =< aux(76)
s(1365) =< aux(74)
s(1367) =< aux(75)
s(1368) =< s(1362)
s(1369) =< s(1363)
s(1367) =< s(1363)
s(1370) =< s(1364)
s(1371) =< aux(74)+1
s(1372) =< aux(74)
s(1373) =< aux(74)-1
s(1365) =< s(1366)+aux(74)
s(1370) =< s(1366)* (1/3)+s(1364)
s(1368) =< s(1366)* (1/2)+s(1362)
s(1370) =< s(1366)* (1/2)+s(1362)
s(1374) =< s(1365)*s(1371)
s(1375) =< s(1365)*s(1372)
s(1376) =< s(1370)*s(1371)
s(1377) =< s(1370)*s(1372)
s(1378) =< s(1368)*s(1372)
s(1379) =< s(1368)*s(1373)
s(1380) =< s(1368)*aux(74)
s(1381) =< s(1374)
s(1382) =< s(1375)
s(1383) =< s(1376)
s(1384) =< s(1377)
s(1385) =< s(1380)
s(1386) =< s(1378)
s(1387) =< s(1379)
s(1390) =< aux(74)
with precondition: []
Closed-form bounds of start(V,V3,V4):
-------------------------------------
* Chain [58] with precondition: []
- Upper bound: nat(V)*29+491+nat(V)*28*nat(V)+nat(V)*56*nat(2/3*V)+nat(V)*30*nat(V/2)+nat(V3)*393+nat(V3)*392*nat(V3)+nat(V3)*784*nat(2/3*V3)+nat(V3)*420*nat(V3/2)+nat(V4)*587+nat(V4)*504*nat(V4)+nat(V4)*1008*nat(2/3*V4)+nat(V4)*540*nat(V4/2)+nat(nat(V)+ -1)*26*nat(V/2)+nat(nat(V3)+ -1)*364*nat(V3/2)+nat(nat(V4)+ -1)*468*nat(V4/2)+nat(2/3*V)*82+nat(2/3*V3)*1148+nat(2/3*V4)*1476+nat(V+1)*45+nat(V3+1)*629+nat(V4+1)*815+nat(V/2+1/2)*17+nat(V3/2+1/2)*238+nat(V4/2+1/2)*306+nat(V/2)*37+nat(V3/2)*518+nat(V4/2)*666
- Complexity: n^2
### Maximum cost of start(V,V3,V4): nat(V)*29+491+nat(V)*28*nat(V)+nat(V)*56*nat(2/3*V)+nat(V)*30*nat(V/2)+nat(V3)*393+nat(V3)*392*nat(V3)+nat(V3)*784*nat(2/3*V3)+nat(V3)*420*nat(V3/2)+nat(V4)*587+nat(V4)*504*nat(V4)+nat(V4)*1008*nat(2/3*V4)+nat(V4)*540*nat(V4/2)+nat(nat(V)+ -1)*26*nat(V/2)+nat(nat(V3)+ -1)*364*nat(V3/2)+nat(nat(V4)+ -1)*468*nat(V4/2)+nat(2/3*V)*82+nat(2/3*V3)*1148+nat(2/3*V4)*1476+nat(V+1)*45+nat(V3+1)*629+nat(V4+1)*815+nat(V/2+1/2)*17+nat(V3/2+1/2)*238+nat(V4/2+1/2)*306+nat(V/2)*37+nat(V3/2)*518+nat(V4/2)*666
Asymptotic class: n^2
* Total analysis performed in 4807 ms.